A, B:MsgA, x:Id. A || B  ma-init-const(A;x)  ma-init-const(B;x)  ma-init-const(A  B;x) 

latex

Definitions

M1  M2, mk-ma, ma-init-const(M;x), MsgA, M.ds(x), Valtype(da;k), M1 || M2, M1 ||decl M2, constant_function(f;A;B), z != f(x)  P(a;z), P  Q, False, x:A.B(x), left + right, Unit, P  Q, P & Q, x:A  B(x), x  dom(f), a:A fp B(a), x. t(x), x.A(x), , , b, A, b, t  T, x:A. B(x), s = t, Top, f  g, IdDeq, <a, b>, f(a), f(x), f(x)?z, Void, Type, , Id, P  Q, x:AB(x), case b of inl(x) => s(x) | inr(y) => t(y), SQType(T), {T}, s ~ t, x,y:A//B(x;y), if b then t else f fi , f || g, Atom$n, f  g, Dec(P),

Lemmas

fpf-sub-join-right, decidable assert, fpf-sub-join-left, subtype-fpf-cap-void, fpf-ap wf, subtype rel self, fpf-join-cap-sq, subtype-fpf-cap-top, assert wf, not wf, bnot wf, bool wf, Id wf, id-deq wf, fpf-cap wf, rationals wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-join-ap-sq, fpf-join-dom2, top wf, fpf-join wf, msga wf, ma-compatible wf, ma-init-const wf